T. Kurahashi, "The provability logic of all provability predicates"
https://arxiv.org/abs/2208.03553
著者
倉橋 太志
Abstract
We prove that the provability logic of all provability predicates is exactly Fitting, Marek, and Truszczyński's pure logic of necessitation N. Moreover, we introduce three extensions N4, NR, and NR4 of N and investigate the arithmetical semantics of these logics. In fact, we prove that N4, NR, and NR4 are the provability logics of all provability predicates satisfying the third condition D3 of the derivabiity conditions, all Rosser's provability predicates, and all Rosser's provability predicates satisfying D3, respectively.
Pure Logic of Necessitation$ \sf N及びその拡張$ \sf N4,NR,NR4での算術的意味論についての研究．
以下を示した．　
次の証明可能性論理と可証性述語が対応する．
$ \sf Nは導出可能性条件D1を満たす証明可能性述語
$ \sf N4は導出可能性条件のD3を満たす証明可能性述語
$ \sf NRはRosser証明可能性述語
$ \sf NR4は導出可能性条件のD3を満たすRosser証明可能性述語．
memo
その他のPure Logic of Necessitationの有限フレーム性についてはT. Kurahashi, Y. Sato; "The finite frame property of some extensions of the pure logic of necessitation"参照．
Introduction
$ Tを算術の言語$ \mathscr{L}_\mathrm{A}上の$ \sf PAの原始再帰的拡大理論とする．
$ Tの証明可能性述語が導出可能性条件のD2とD3と満たせばGödelの第2不完全性定理が成り立つ．
すなわち，$ \mathrm{Pr}_T(x)が
D2. $ T \vdash \mathrm{Pr}_T(\ulcorner \varphi \to \psi \urcorner) \to (\mathrm{Pr_T(\ulcorner \varphi \urcorner )} \to \mathrm{Pr_T(\ulcorner \psi \urcorner )})
D3. $ T \vdash \mathrm{Pr_T(\ulcorner \varphi \urcorner )} \to \mathrm{Pr_T(\ulcorner Pr_T(\ulcorner \varphi \urcorner ) \urcorner )}
を満たせば$ T \nvdash \lnot\mathrm{Pr}_T(\ulcorner 0=1 \urcorner)
SnO2WMaN.iconD1は？
D2とD3が成り立つ可証性述語$ \mathrm{Pr}_T(x)をここでは$ \mathrm{Prov}_T(x)とする．
$ T \nvdash \mathrm{Prov}_T(\ulcorner 0 = 1 \urcorner)
Robert M. SolovayによるSolovayの算術的完全性定理の成果の結果
$ \Boxを$ \mathrm{Pr}_Tと考える証明可能性論理において
$ TがΣ₁健全なら，$ \mathrm{Prov}_Tについての論理は様相論理GLと一致する．
Robert M. Solovay; 1976; "Provability Interpretation of Modal Logic"参照．
が，全ての証明可能性論理が$ \sf GLと一致するわけでもない．
第2不完全性定理を導かない可証性述語の証明可能性論理について
例えばRosser証明可能性述語$ \mathrm{Pr}^\mathrm{Ro}_Tについて
Kreiselの注意．$ T \vdash \lnot\mathrm{Pr}^\mathrm{Ro}_T(\ulcorner 0 = 1 \urcorner)
このとき$ \sf GLでは矛盾する$ \lnot\Box\botが導かれるのでおかしい．
なぜこうなるのか？
Rosser証明可能性述語の構成方法によっては，D2またはD3の少なくともどちらか片方は満たさない．
remark:
D2. $ \Box(A \to B) \to (\Box A \to \Box B)
remark:様相論理の公理K．
D3. $ \Box A \to \Box\Box A
remark:ネセシテーションの特殊例．
参考
D2,D3のどちらもも満たさないRosser証明可能性述語については
D. Guaspari, Robert M. Solovay, "Rosser sentences"
D2だけを満たすRosser証明可能性述語については
C.Bernardi, F. Montagna, "Equivalence relations induced by extensional formulae: classification by means of a new fixed point property"
T. Arai; "Derivability conditions on Rosser's provability predicates"
D3だけを満たすRosser証明可能性述語
T. Arai; "Derivability conditions on Rosser's provability predicates"
D2を満たすRosser証明可能性述語についての論理は正規様相論理KDとして特徴づけることが出来る．
remark:$ \mathsf{KD} = \mathsf{K} + \lnot\Box\bot
T. Kurahashi, "Rosser Provability and Normal Modal Logics"参照．
D3を満たす（D2を満たさない）Rosser証明可能性述語は$ \sf Kを含まないので，正規様相論理ではない．
$ \Sigma_1でない$ Tの可証性述語についての証明可能性論理も$ \sf GLと一致しない．
$ Tの$ \Sigma_2可証性述語は最弱の正規様相論理$ \sf Kと一致する．（正規様相論理K）
T. Kurahashi, "Arithmetical completeness theorem for modal logic K"
その他の$ \Sigma_2可証性述語に対応する正規様相論理は下記参照．
T. Kurahashi, "Arithmetical soundness and completeness for Σ₂ numerations"
F. Montagna, "On the algebraization of a Feferman’s predicate"
V. Yu. Shavrukov, "A smart child of Peano’s"
A. Visser, "Peano’s smart children: A provability logical study of systems with built-in consistency"
Q1. 全ての可証性述語に共通する証明可能性論理は何か？すなわち，全ての証明可能性論理の共通部分は何か？
Q2. 全てのRosser可証性述語の証明可能性論理は何か？
可証性述語の共通してあるべき性質は↓の性質であろう．
導出可能性条件 D1. $ T \vdash \varphi \implies T \vdash \mathrm{Pr}_T(\ulcorner \varphi \urcorner)
これはネセシテーションに対応する．すなわち$ A \mid \Box A．
となると，Pure Logic of Necessitationを持ち出してみようということになる．
Pure Logic of Necessitation$ \sf Nとは古典命題論理にネセシテーションだけを追加した非正規様相論理である．
すなわちKripkeモデルを用いた意味論は使えない．
が，Solovayの算術的完全性定理の証明にはKripkeモデルを算術を埋め込む必要がある．
これは正規様相論理を元にした証明可能性論理なら上手く行くが…
Pure Logic of Necessitationの擬Kripkeモデルの健全性，完全性，有限フレーム性はM.C.Fitting, V.W.Marek, M.Truszczyński; "The pure logic of necessitation"によって示されている．　
これに対してSolovayの算術的完全性定理のテクニックを使うと上手く行く．
これによってQ1が解決される．Sect4.
さらに言えばPure Logic of Necessitation Nに対応する$ \Sigma_1可証性述語が存在することも明らかになる．Appendix1.
$ \sf NRとは$ \sf NにRosser推論規則$ \lnot\varphi \mid \lnot\Box\varphiを追加したものである．
これにも有限フレーム性がある．
Sect6.で$ \sf NRは全てのRosser証明可能性述語の証明可能性論理となることを示す．
これによってQ2が解決される．
$ \sf N,NRに様相論理の公理4$ \Box A \to \Box\Box Aを追加した$ \sf N4,NR4について
これにも有限フレーム性がある．
Sect5. $ \sf N4は導出可能性条件D3を満たす全ての可証性述語の証明可能性論理になる．
Sect7. $ \sf NR4は導出可能性条件D3を満たす全てのRosser証明可能性述語の証明可能性条件になる
Appendix2.$ \sf NRの$ \Box,\Diamondの相互交換性について議論する.
これは推論規則として$ A \to B \mid \Box A \to \Box Bが追加された非標準様相論理に繋がっていく．
H. Kogure, T. Kurahashi, "Arithmetical completeness theorems for monotonic modal logics"参照（未出版？）
Sect 2.